x, y:. (x = (y))  ((x = y)) 

latex

ProofTree

Definitions	b, , A, Void, x:AB(x), P  Q, False, P  Q, x:A  B(x), P & Q, P  Q, s = t, t  T, x:A. B(x), p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, f(a), x f y, a < b, b, p  q, p  q, p q, Type, , ff, tt, , Unit, left + right, Dec(P), P  Q
Lemmas	decidable assert, iff transitivity, btrue wf, bfalse wf, eqtt to assert, bool wf, eqff to assert, bnot wf, iff functionality wrt iff, iff wf, rev implies wf, not functionality wrt iff, assert of bnot, not wf, assert wf